(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun e () String)
(declare-fun f () String)
(declare-fun g () String)
(assert (= g (str.++ e f)))
(assert (= c d 20))
(assert (distinct a d (str.len g)))
(assert (= c (str.len e)))
(check-sat)
